ds:x:Id fp Type, da:k:Knd fp Type, i:Id, es:ES.
(x:Id. vartype(i;x)  ds(x)?Top)
 (e:E. loc(e) = i  valtype(e)  da(kind(e))?Top)
 (e1, e2, e3:E.
 (loc(e1) = i
 ( e1  e2 
 ( e1  e3 
 ( es-hist{i:l}(es;e1;e2) = es-hist{i:l}(es;e1;e3)  event-info(ds;da) List
 ( e2 = e3) 

latex

Definitions	Id, t  T, x. t(x), x:A. B(x), a:A fp B(a), Knd, ES, Top, IdDeq, vartype(i;x), f(x)?z, kind(e), KindDeq, valtype(e), loc(e), P  Q, E, Prop, e  e' , b, False, A, es-hist{i:l}(es;e1;e2), event-info(ds;da), ||as||, [e, e']
Lemmas	length-map, es-interval wf, length wf1, es-interval-length-one-one, event-info wf, es-hist wf, es-le-loc, es-loc-pred, es-le wf, es-E wf, es-loc wf, es-valtype wf, Kind-deq wf, es-kind wf, es-vartype wf, fpf-cap wf, id-deq wf, top wf, event system wf, Knd wf, fpf wf, Id wf